FDL - Nuprl Lemma : anti_sym_functionality_wrt_iff

Nuprl Lemma : anti_sym_functionality_wrt_iff

T:Type, R, R':(T

T

).
(

x, y:T. R(x,y)

R'(x,y))

(AntiSym(T;x,y.R(x,y))

AntiSym(T;x,y.R'(x,y)))

Up rel 1, rel 1

Definitions P Q, P & Q, P Q, t T, x(s1,s2), P Q, x:A. B(x),

Lemmas iff wf